#include "clause.h"
#include "common.h"
#include<stddef.h>
#include<stdio.h>
#include "var.h"
variable __variables[MAX_TOT_VAR];
int _clause_start[MAX_TOT_VAR];
int _clause_varn[MAX_TOT_VAR];

_bool clause_is_true(clause* cl){
    int i;
#ifdef __serial
    //if(cl->true_val_available && cl->true_val) return true;
    // a clause is true if one of it's real values is true
    for(i = 0; i < cl->var_num; i++){
        if(get_vflag((cl->vars + i), assigned) && get_real_value(cl->vars + i)){
            return true;
        }
    }
    return false;
#endif
#ifdef __vector //for 3sat problem doesn't worth it
    if(cl->true_val_available && cl->true_val) return true;
    // a clause is true if one of it's real values is true
    for(i = 0; i < cl->var_num; i++){
        if(get_vflag((cl->vars + i), assigned) && get_real_value(cl->vars + i)){
            return true;
        }
    }
    return false;
#endif
    assert(0);
}

_bool clause_is_false(clause* cl){
#ifdef __serial
    int i;
    // all variables have to be assigned
    for(i = 0; i < cl->var_num; i++){
        if(!get_vflag((cl->vars + i), assigned)){
            return false;
        }
    }
    // if all are assigned, all real values have to be false
    for(i = 0; i < cl->var_num; i++){
        if (get_real_value(cl->vars + i)){
            return false;
        }
    }
    return true;
#endif
#ifdef __vector
    int i;
    // all variables have to be assigned
    for(i = 0; i < cl->var_num; i++){
        if(!get_vflag((cl->vars + i), assigned)){
            return false;
        }
    }
    // if all are assigned, all real values have to be false
    for(i = 0; i < cl->var_num; i++){
        if (get_real_value(cl->vars + i)){
            return false;
        }
    }
    return true;
#endif
    assert(0);
}


void print_clause(clause* cls){
    assert(cls != NULL && cls->var_num > 0);
    printf("num: %d {", cls->var_num);
    for(int i = 0; i < cls->var_num; i++){
        // printf("@\n");
        printf("(name:%d,sign: %d,",cls->vars[i].name, cls->vars[i].sign);
        if (cls->vars[i].assigned){
            printf("value:%d),", cls->vars[i].value);
        }
        else{
            printf("unassigned),");
        }
    }
    printf("}, \n");
}

void delete_clause(clause* cls){
    if (cls == NULL){
        return;
    }
    free(cls->vars);
    free(cls);
}